COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	bird.2[f82,jmc]		Another approach to " A bird can fly unless
C00006 00003	Circumscribing two sentences
C00012 00004	A[P]
C00013 ENDMK
C⊗;
bird.2[f82,jmc]		Another approach to " A bird can fly unless

	In this article we shall show how to construct a data base of
first order sentences in mathematical logic expressing some common sense
facts about which animals can fly.  New information, such as the
fact that ostriches can't fly, can be added to the data base without
changing existing sentences.  Our main tool is an improved version of
the circumscription method of non-monotonic reasoning described in
(McCarthy 1980).

	The basic idea can be summarized very simply.  The key sentence is

(1)	∀x. is-bird x ∧ ¬nnly-can-fly x ⊃ can-fly x,

which is taken as asserting that a bird can fly unless the predicate
nnly-can-fly  applies to it.  nnly  stands for "not necessarily" but
shouldn't be identified with any modal operator.
  Non-standard birds are then separated out
by sentences like

(2)	∀x. is-ostrich x ⊃ nnly-can-fly x

and

(3)	∀x. dead x ⊃ nnly-can-fly x.

Circumscription is used to express the assumption that  nnly-can-fly x
is true only when this follows from the facts known about  x.  This
permits inferring that Tweety, a canary (not known to be dead),
can fly without permitting the
inference that Joe, an ostrich, can fly.

	Reiter's (1979) "closed world assumption" is that all predicates
in a data base have the minimal extension compatible with the facts
asserted about them.  This turns out to be an over-simplification, and
the present problem requires that the common sense data base contain
information that minimizes some predicates at the expense of others.
I think such additional information will be wanted regardless of whether
circumscription or some other formalism is used to do the non-monotonic
reasoning.  Notice that (1) can be written

(1')	∀x. is-bird x ⊃ nnly-can-fly x ∨ can-fly x,

which is symmetrical in the predicates  nnly-can-fly  and  can-fly.
Inferring that Tweety can fly requires minimizing  nnly-can-fly
with higher priority than minimizing  can-fly.  This corresponds
to the common sense intuitions that we are trying to capture.  We
might do it by including a partial ordering of
predicate symbols in the common sense data base.  However, the relative
priority of the expressions being minimized may itself be the
result of reasoning.
  Part of the
extension to the previous concept of circumscription is concerned with
how this partial ordering is used.
Circumscribing two sentences

	There are two ways of circumscribing two sentences together - in
serial, with one sentence having higher "priority" or in parallel.

	Serial circumscription involves 
minimizing the second sentence using what variability is
left over after minimizing the first.
Thus let the sentences be  E[P1,...,Pn,x]  and  F[P1,...,Pn,x],
where  x  is the variable of quantification and the  Pi  are to be chosen so as
achieve the minimization.  Also suppose that the  Pi  are required to
satisfy the axiom  A[P1,...,Pn].

	In order to shorten the formulas we exhibit
the case where there is only one  P.  We first make the definition

b1: A'[P] ≡ A[P] ∧ (∀P'.A[P'] ∧ (∀x.E[P',x] ⊃ E[P,x]) ⊃ (∀x.E[P,x] ⊃ E[P',x])),

after which

b2: A'[P] ∧ (∀P'.A'[P'] ∧ (∀x.F[P',x] ⊃ F[P,x]) ⊃ (∀x.F[P,x] ⊃ F[P',x]))

is the circumscription formula itself.
Namely  A'[P]  is the usual circumscription of  E[P,x], and the second
part of  b2 states that among the predicates  P'  that satisfy  A'[P'],
P  minimizes  F[P,x].

	The corresponding parallel circumscription of  E[P,x]  and
F[P,x]  is given by the formula

b4:	A[P] ∧ ∀P'.A[P'] ∧ (∀x.E[P',x] ⊃ E[P,x]) ∧ (∀x.F[P',x] ⊃ F[P,x])
		⊃ (∀x.E[P,x] ⊃ E[P',x]) ∧ (∀x.F[P,x] ⊃ F[P',x]).

	In the bird example, serial circumscription is appropriate.
In a shortened version of the facts, suppose we take
into account only the conjunction

b3:	∀x.is-bird x ∧ ¬nnly-can-fly x ⊃ can-fly x
	∧ ∀x.is-ostrich x ⊃ nnly-can-fly x.

We want to circumscribe

b5:	E[nnly-can-fly,can-fly,x] ≡ nnly-can-fly x

and

b6:	F[nnly-can-fly,can-fly,x] ≡ can-fly x

with the former taking priority.  We have

b7: A[nnly-can-fly, can-fly] ≡ (∀x.is-bird x ∧ ¬nnly-can-fly x ⊃ can-fly x)
		∧ (∀x.is-ostrich x ⊃ nnly-can-fly x),

and the predicates  nnly-can-fly  and  can-fly  are the variables.
We then have the definition

b8: A'[nncf,cf] ≡ (∀x.is-bird x ∧ ¬nncf x ⊃ cf x) ∧ (∀x.is-ostrich x ⊃ nncf x)
	∧ ((∀nncf' cf'.(∀x.is-bird x ¬nncf' x ⊃ cf' x) ∧ (∀x.is-ostrich x ⊃ nncf' x)
		∧ (∀x.nncf' x ⊃ nncf x) 
			⊃ (∀x.nncf x ⊃ nncf' x)))

and the circumscription formula

b9:	A'[nnly-can-fly,can-fly]
∧ (∀nncf cf.A'[nncf,cf] ∧ (∀x.cf x ⊃ can-fly x) ⊃ (∀x.can-fly x ⊃ cf x)).

	The first two conjuncts of  A'[nnly-can-fly,can-fly]  is the axiom
b3, so this gives nothing new.  We specialize the remaining conjunct
by substituting  is-ostrich  for nncf'  and  λx.is-bird x ∧ ¬is-ostrich x
for  cf'.  This makes the conjunct into

b10:	(∀x.is-bird x ∧ ¬is-ostrich x ⊃ is-bird x ∧ ¬is-ostrich x)
	∧ (∀x. is-ostrich x ⊃ is-ostrich x)
	∧ (∀x. is-ostrich x ⊃ nnly-can-fly x)
	⊃ (∀x. nnly-can-fly x ⊃ is-ostrich x).

	The premisses of b10 are all true, so we get

b11:	∀x.nnly-can-fly x ⊃ is-ostrich x,

and using the second conjunct of b3 gives

b12:	∀x.nnly-can-fly x ≡ is-ostrich x.

	We now subsitute  is-ostrich  for  nncf  and
λx.is-bird x ∧ ¬is-ostrich x  for  cf  in the second part of  b9 getting
finally

b13:	∀x.can-fly x ⊃ is-bird x ∧ ¬is-ostrich x,

after observing that the premisses of the implication follow easily.

	Thus taking into account only b3 leads circumscriptively
to the conclusion that the only things that can fly are birds that are
not ostriches.  This is the result we want.
A[P]
∧ ∀Q.{A[Q] ∧ (∀x.E[Q,x] ⊃ E[P,x]) ⊃ (∀x.E[P,x] ⊃ E[Q,x])
∧ ∀R.A[R] ∧ (∀Q.{A[Q] ∧ (∀x.E[Q,x] ⊃ E[R,x]) ⊃ (∀x.E[R,x] ⊃ E[Q,x]))
∧ ∀x.(F[R,x] ⊃ F[P,x])
	⊃ ∀x.(F[P,x] ⊃ F[R,x])